\subsection{Termination in CCS}
\newcommand{\dnew}{d_p}
\newcommand{\pn}{pn}
\newcommand{\oldderiv}[1]{\pired^{#1}}
\newcommand{\procleq}{\preceq}
\newcommand{\subp}{\mathit{Sub}}
\newcommand{\PPn}{{\cal P}_{P,n}}
\newcommand{\PPnmenouno}{{\cal P}_{P,n-1}}
\newcommand{\PPzero}{{\cal P}_{P,0}}
\newcommand{\PPdP}{{\cal P}_{P,\dnew(P)}}


\subsubsection{Termination is decidable in $\ccsb$}



%The last, and more complex, step in order to prove that termination is decidable for $(\ccsb, \oldderiv{})$ is to equip the transition system $(\ccsbang, \deriv{})$ with a well-quasi-order compatible with $\deriv{}$.
%The desired result then follows from  Theorem~\ref{divdec} and Corollary \ref{cor:eqterm}. 

%To define the well-quasi-order we first introduce another congruence con processes, which is simpler than $\equiv_T$ and which turns out to be compatible with $\deriv{}$. In fact, differently from the case of the previous section, here the congruence is needed only to simplify the definition of the quasi-order, hence we do not need to take into account the replication operator. 

% \begin{definition}
% We define $\strucong$ as the least congruence relation satisfying
% the following axioms:\ \ \ \ \ \ \
% \[\begin{array}{l}
% P | Q \strucong Q | P \ \ \ \ \ 
% \\
% P | (Q | R) \strucong (P | Q) | R \ \ \ \ \  
% \\
% P | \nullo \strucong P
% \end{array}\]
% \end{definition}


We can now define  the relation $\procleq$ which will be proven to be a well-quasi-order.


\begin{definition}\label{procleq}
Let $P, Q\in\ccsb$.
We write
$P\procleq Q$ iff there exist $n$, $a_1,\ldots, a_n$, $P'$, $R$, $P_1,\ldots, P_n$,
$Q_1,\ldots, Q_n$ such that

$P \equiv P' \parallel  \prod_{i=1}^{n} \pass{a_i}{P_i}$,
\\
$Q\equiv P' \parallel R \parallel \prod_{i=1}^{n} \pass{a_i}{Q_i}$, and 
%\item
$P_i\procleq Q_i$ for $i= 1,\ldots, n$.
%\]
%\end{itemize}
\end{definition}

Intuitively $P\procleq Q$ holds if $Q$ can be obtained, up to $\equiv$, from $P$ by adding some parallel processes while preserving the nesting structure given by passivation units. 
In order to show that  the relation $\procleq$ is indeed a quasi order 
we need some more notation and a preliminary lemma.

First  we define the maximum number $\dnew(P)$ of nested passivation in a process $P$.
\begin{definition}
Let $P\in\ccsb$. We define  $\dnew(P)$  inductively as follows:
\[
\begin{array}{l}
\dnew(a.P) = \dnew(P) \\
\dnew(\outC{a}) = 0 \\
\dnew(P \parallel Q) = max(\{\dnew(P), \dnew(Q)\}) \\
\dnew(\pass{a}{P}) = 1 + \dnew(P) \\
\dnew(!P) = \dnew(P)
\end{array}
\]
\end{definition}

Then we need also a notation for indicating all the sequential and bang subprocesses of 
$P$.
\begin{definition}
Let $P\in\ccsb$. The set $\subp(P)$ containing all the sequential and bang subprocesses of $P$ is defined inductively as follows:
\[
\begin{array}{l}
\subp(a.P) = \{a.P\}\cup \subp(P) 
\\
\subp(\outC{a}) = \{a\} \\
\subp(P \parallel Q) = \subp(P)\cup\subp(Q) \\
\subp(\pass{a}{P}) = \subp(P) \\
\subp(!P) = \{!P\}\cup\subp(P)
\end{array}
\]
\end{definition}

We shall need the following auxiliary definition:

\begin{definition}[Passivation Names]
Let $P\in\ccsb$. The set $\pn(P)$ containing all the names of passivation units of $P$ is defined inductively as follows:
\[
\begin{array}{l}
\pn(a.P) = \pn(P) \\
\subp(\outC{a}) = \emptyset \\
\subp(P \parallel Q) = \pn(P)\cup\pn(Q) \\
\subp(\pass{a}{P}) = \{a\} \cup \pn(P) \\
\subp(!P) = \pn(P)
\end{array}
\]
\end{definition}

Finally with $\PPn$ we denote
the set of all those $\ccsb$ processes whose nesting level of passivation units is not greater than $n$ and such that their
sequential subprocesses, bang subprocesses and passivation names are contained in the corresponding elements of $P$. 

More precisely we have the following definition.


\begin{definition}[$\PPn$]\label{def:ppn}
Let $n$ be a natural number and $P$ a process.
We define $\PPn$ as follows:

\[\PPn = \{Q\in\ccsb \mid
\subp(Q) \subseteq\subp(P)\wedge
\pn(Q)\subseteq \pn(P)\wedge
\dnew(Q)\leq n\}\]
\end{definition}

The notion of $\PPn$ is important because 
processes contained in $\PPn$ can be written
in a sort of normal form (up to $\equiv$) which allows us to simplify the proofs. This is the content of the following lemma.


\begin{lemma}\label{normform}
Let $P\in\ccsb$, $n\leq\dnew(P)$ and $Q\in\PPn$.
Suppose that $| \pn(P) | = m$ and $\pn(P) = \{a_1,\ldots, a_m\}$.
Then there exist $l$,  $k_1,\ldots, k_m$ such that
\[Q\equiv 
\prod_{i=1}^{l} Q_i | 
 \prod_{j=1}^{m} (\prod_{h=1}^{k_j} \pass{a_j}{R_{j,h})}\]
for some 

$Q_i\in\subp(P)$ for $i= 1,\ldots, l$

$R_{j,h}\in\PPnmenouno$ for $j=1,\ldots, m$ (and corresponding $h=1,\ldots k_j$)
\end{lemma}
\begin{proof}
By induction on the structure of Q.
\end{proof}

Using this normal form we can prove that $\procleq$ is a quasi order.

\begin{proposition}
The relation $\procleq$ is a quasi order over $\ccsb$ processes.
\end{proposition}
\begin{proof}
Transitivity of $\procleq$ is a consequence of the following fact.

If $P\procleq Q$, by definition of $\procleq$
and by Lemma~\ref{normform} it follows that that
\[P\equiv
\prod_{i=1}^{l} P_i \parallel 
\prod_{j=1}^{m}\prod_{h=1}^{k_{j}} \pass{a_j}{R_{j,h}}\]
and
\[Q\equiv
\prod_{i=1}^{l+l'} P_i \parallel
\prod_{j=1}^{m}\prod_{h=1}^{k_{j}+k'_{j}} \pass{a_j}{R'_{j,h}}
\]
with $P_i\in\subp(P|Q)$ for $i=1,\ldots, l+l'$ and
$R_{j,h}\procleq R'_{j,h}$ for $j=1,\ldots, m$ 
(and corresponding $h= 1,\ldots, k_{j}$).
\end{proof}



To prove that $\procleq$ is a well-quasi-order we need two more
preliminary results. The first, rather obvious, states that the set of sequential and bang subprocesses of a process is finite. 
\begin{proposition} \label{subpfinite}
Given a process $P\in\ccsb$ the set $\subp(P)$ is finite.
\end{proposition}
\begin{proof}
By induction on the structure of $P$.
\end{proof}

The second one shows that when performing a derivation step we obtain a process which is not more ``complicated'' than the original one. This is an important feature of $\ccsb$ which is due to the absence of recursive definitions. Essentially this is the  key property that allows us to obtain the decidability of termination.

\begin{proposition}\label{prop:keyfeature}
Let $P\in\ccsb$ and $Q\in\PPn$.
If $Q\oldderiv{} Q'$ then $Q'\in\PPn$.
\end{proposition}
\begin{proof}
By induction on the proof of $Q\oldderiv{} Q'$, with a case analysis on the last applied rule.
We concentrate in the case of rule \textsc{Tau1}.
There are several cases depending on the synchronization partners.
\begin{enumerate}
 \item Input/Output synchronization: Then $Q \equiv a.Q_1 \parallel \outC{a}$ and
$Q' \equiv Q_1$, and the thesis follows from the definition.
%(The case $Q \equiv \outC{a} \parallel a.Q_1 \parallel $

\item Input/Suspension synchronization: Then $Q \equiv a.Q_1 \parallel \pass{a}{Q_2}$
and $Q' \equiv Q_1$, and the thesis follows.

\item Synchronization inside a passivation unit: Then $Q \equiv \pass{a}{Q_1} \parallel Q_2 $
with $Q_1 \oldderiv{\alpha} Q'_1$ and $Q_2 \oldderiv{\outC{\alpha}} Q'_2$.
Hence, $Q' \equiv \pass{a}{Q'_1} \parallel Q'_2$, as depicted below:
\[
\cfrac{\cfrac{Q_1 \oldderiv{\alpha} Q'_1}{\pass{a}{Q_1} \oldderiv{\alpha} \pass{a}{Q'_1}} \quad Q_2 \oldderiv{\outC{\alpha}} Q'_2}{
\pass{a}{Q_1} \parallel Q_2 \oldderiv{} \pass{a}{Q'_1} \parallel Q'_2
}
\]
By inductive hypothesis we know that $\pass{a}{Q'_1}$ and $Q'_2$ belong to $\PPn$.
Then their parallel composition is also in $\PPn$ and we are done.
\end{enumerate}
\end{proof}

\begin{myrem}
Notice that this property only holds because passivation as defined in \ccsb destroys the 
content of the passivation unit. This is not the case of passivation in higher-order process calculi, as we shall see later.
\end{myrem}


An immediate consequence of the above proposition is that all the processes 
reachable from $P$ with a sequence of reduction steps  belong to $\PPn$, where $n$ is the maximum level of nesting of $P$. 
We state this fact as an explicit corollary since we will need it later. So, we denote by $Deriv(P)$ the processes reachable from $P$ with a sequence of reduction steps. 

\begin{definition}
Let $P\in\ccsb$. Then we define
\[Deriv(P) = \{Q\mid P\oldderiv{*} Q\}\]
\end{definition}

Then we have the following.

\begin{corollary}\label{derivsubseteqPPn}
Let $P\in\ccsb$. 
Then $Deriv(P)\subseteq {\cal P}_{P,\dnew(P)}$ holds.
\end{corollary}
\begin{proof}
Immediate from Proposition \ref{prop:keyfeature}.
\end{proof}


Now we are ready to prove that $\procleq$ is a well-quasi-ordering.
The key idea is the following: we use Lemma~\ref{normform}
to transform each derivative of $P$ in $1 + m$ (finite) sequences,
where $m$ is the cardinality of $\pn(P)$.
The first sequence is over $\subp(P)$ which is a finite set, whereas
the other sequences are over processes that are ``simpler'' than $P$,
in the sense that the nesting level of passivation units in those processes is
strictly smaller  than $\dnew(P)$.
The result is proved proceeding by induction on the nesting level of 
passivation units and using the Higman's lemma.

\begin{theorem} \label{procleqwqo}
Let $P\in\ccsb$ and $n\geq 0$.
The relation $\procleq$ is a wqo over $\PPn$.
\end{theorem}
\begin{proof}
The proof is by induction on $n$.

Let $n = 0$.
\\
Take an infinite sequence $P_1, P_2,\ldots, P_i,\ldots$, with $P_i\in\PPzero$ for $i>0$.
\\
By Lemma~\ref{normform}, for any $i$ we have that $P_i \equiv \prod_{j=1}^{n_i} P_{i,j}$,
with $P_{i,j}\in\subp(P)$.
\\

--- CHECK REFERENCES TO FINKEL ---

Hence, we have an infinite sequence of elements of $\subp(P)^{*}$; 
as $\subp(P)$ is finite (by Proposition~\ref{subpfinite}), by Proposition~\ref{wqofinite} and Higman's
Lemma (Lemma \ref{higman}) we have that $=_{*}$ is a wqo over $\subp(P)^{*}$ 
(the relation $=_{*}$ on sequences is defined according to Definition \ref{def:*}, where we consider equality as the quasi order on the starting set).
\\
It's easy to see that if $P_{i,1} P_{i,2} \ldots P_{i,n_i} =_{*} P_{k,1} P_{k,2} \ldots P_{k,n_k}$
then $P_{i}\procleq P_{k}$.

For the inductive step, let $n>0$ and take an infinite sequence $P_1, P_2,\ldots, P_i,\ldots$, with 
$P_i\in\PPn$ for any $i>0$.
\\
By Lemma~\ref{normform}, there exists $m$ such that, for any $i$ we have that
\[P_i \equiv \prod_{j=1}^{n_i} P_{i,j}| 
\prod_{j=1}^{m}\prod_{h=1}^{k_{i,j}} \pass{a_j}{ R_{i,j,h}}
\]
with $P_{i,j}\in\subp(P)$ and $R_{i,j,h}\in\PPnmenouno$.
\\
Hence, each $P_i$ can be seen as composed of $m + 1$ finite sequences:
\[
\begin{array}{l}
P_{i,1} \ldots P_{i,n_i}
\\
R_{i, 1, 1} \ldots R_{i, 1, k_{i,1}}
\\
\vdots
\\
R_{i, m, 1} \ldots R_{i, m, k_{i,m}}
\end{array}
\]
We note that the first sequence is composed of elements from the finite set $\subp(P)$,
whereas the other $m$ sequences are composed of elements in $\PPnmenouno$.
We know from the base case that $=_{*}$ is a wqo over $\subp(P)^{*}$.
\\
By inductive hypothesis, we have that $\procleq$ is a wqo on $\PPnmenouno$;
hence, by Higman's Lemma we have that $\procleq_{*}$ is a wqo on 
$\PPnmenouno^{*}$.
\\
We start extracting an infinite subsequence from $P_{1}\ldots P_{i}\ldots$ making
the finite sequences $P_{i,1} \ldots P_{i,n_i}$ increasing w.r.t. $=_{*}$;
then, we extract an infinite subsequence from the subsequence obtained in the
previous step, that makes the finite sequences $R_{i, 1, 1} \ldots R_{i, 1, k_{i,1}}$
increasing w.r.t. $\procleq_{*}$, and so on.
\\
%It's easy to see that a
At the end of the process we obtain an infinite subsequence of 
$P_{1}\ldots P_{i}\ldots$ that is ordered w.r.t. $\procleq$.
\end{proof}


As the last step in order to obtain our decidability result, we need to show that the relation $\procleq$ of Definition~\ref{procleq} is strongly compatible with $\oldderiv{\alpha}$. 
This is the content of theorem \ref{strongcompatibility} below. % which uses the following proposition.

% THIS SHOULD BE DONE BEFORE, ADD REFERENCES.
% 
% \begin{proposition} \label{strucompderiv}
% Let $P, Q\in\ccsbang$.
% If $P\strucong Q$ and $Q\deriv{\alpha} Q'$ then there exists $P'$ such that
% $P\deriv{\alpha} P'$ and $P'\strucong Q'$.
% \end{proposition}
% \begin{proof}
% By induction on the proof of the relation $P\termequiv Q$.
% \end{proof}
% 

\begin{theorem}\label{strongcompatibility}
Let $P, Q, P'\in\ccsb$.
If $P\oldderiv{\alpha} P'$ and $P\procleq Q$ then there exists $Q'$ such
that $Q\oldderiv{\alpha} Q'$ and $P'\procleq Q'$.
\end{theorem}
\begin{proof}
The proof is by induction 
on the proof of $P\oldderiv{\alpha} P'$, with a case analysis on the last applied rule.

By definition of $\procleq$ we have that
$P \equiv \bar{P} | \prod_{i=1}^{n} \pass{a_i}{P_i}$ and
$Q \equiv \bar{P} | R | \prod_{i=1}^{n} \pass{a_i}{Q_i}$, with
$P_i\procleq Q_i$ for $i= 1,\ldots, n$.

We can focus only on the case of \textsc{Tau1} and two situation can occur:
\begin{enumerate}
 \item the synchronization occurs inside $\bar{P}$ then the thesis easily follows by definition of $\procleq$.
 \item the synchronization involves $\pass{a_j}{P_j}$ for some $j$.
The following tree can be built
$$
\rightinfer{\pass{a_j}{P_j} \parallel P_1 \arr\tau  \pass{a_j}{P'_j} \parallel P'_2 }
	   {\pass{a_j}{P_j} \arr{\alpha} \pass{a_j}{P'_j} \andalso P_1 \arr{\bar{\alpha}} P'_1}
$$
Then the thesis easily follows by using the inductive hypothesis and by noticing that $P_j \procleq Q_j$

\end{enumerate}

% 
% 
% First of all, note that $\dnew(P_i) < \dnew(P)$ for $i= 1,\ldots, n$.
% 
% 
% As $P\deriv{\alpha} P'$, by Proposition~\ref{strucompderiv} also
% $\bar{P} | \prod_{i=1}^{n} (\new x_i) P_i\deriv{\alpha}P''$ wih $P''\strucong P'$.
% The proof proceeds by case analysis on the last rule applied in the proof
% of transition $\bar{P} | \prod_{i=1}^{n} (\new x_i) P_i\deriv{\alpha}P''$.
\end{proof}

%Note that the above result implies that $\procleq$ is also strongly compatible
%with $\deriv{}$. ??????????


We can then state the main result of this section.
\begin{theorem}\label{th:main}
Let $P\in\ccsb$.
Then the transition system $(Deriv(P), \oldderiv{}, \procleq)$ is a finitely branching well-structured
transition system with strong compatibility, decidable $\procleq$ and computable $Succ$.
\end{theorem}
\begin{proof}
The fact that $(Deriv(P), \oldderiv{})$ is finitely branching derives from an inspection of the transition rules (in particular {\tt REPL1} and {\tt REPL2}). The fact that $\procleq$ is a well-quasi-order on $Deriv(P)$ is a consequence
of Corollary~\ref{derivsubseteqPPn} and Theorem~\ref{procleqwqo} 
(taking $n=\dnew(P)$). Strong compatibility has been proven in Theorem~\ref{strongcompatibility}.
\end{proof}






%\begin{theorem}\label{wstsproc}
%Let $P\in\ccsbang$.
%Then the transition system $(Deriv(P), \deriv{}, \procleq)$ is a well-structured
%transition system with strong compatibility, decidable $\procleq$ and computable $Succ$.
%\end{theorem}
%%\begin{proof}
%%See Appendix~\ref{decterm}.
%%\end{proof}

\begin{corollary}
Let $P\in\ccsb$.
The termination of process $P$ is decidable.
\end{corollary}
\begin{proof}
Immediate from Theorem \ref{divdec}, Corollary \ref{cor:eqterm} and Theorem \ref{th:main}.
\end{proof}






